ma-interface-consistent2(es;I)
== i:Id.
== (i  ma-interface-locs(I))
==  (k:{k:Knd| hasloc(k;i)} .
==  (k  ma-interface-dom(I;i))
==   (e@i. (kind(e) = k)  (valtype(e) r ma-interface-valtype(I;i;k))
==   & (x:Id. vartype(i;x) r ma-interface-ds(I;i)(x)?Top))) 

latex

---

clarification:

ma-interface-consistent2(es;I)
== i:Id.
== (i  ma-interface-locs(I)  Id)
==  (k:{k:Knd| hasloc(k;i)} .
==  (k  ma-interface-dom(I;i)  Knd)
==   (alle-at(es;i;e.(es-kind(es; e) = k  Knd)
==    (es-valtype(es; e) r ma-interface-valtype(I;i;k)))
==   & (x:Id. es-vartype(es; i; x) r fpf-cap(ma-interface-ds(I;i);IdDeq;x;Top)))) 

latex

Definitions	ma-interface-locs(I), {x:A| B(x)} , b, hasloc(k;i), (x  l), ma-interface-dom(I;i), P & Q, e@i. P(e), P  Q, s = t, Knd, kind(e), valtype(e), ma-interface-valtype(I;i;k), x:A. B(x), Id, vartype(i;x), f(x)?z, ma-interface-ds(I;i), IdDeq, Top
FDL editor aliases	ma-interface-consistent2